“SMT” (Satisfiability Modulo Theories) generalizes Boolean satisfiability (SAT) by adding equality reasoning, arithmetic, fixed-size bit-vectors, arrays, quantifiers, and other useful first-order theories. An SMT solver is a tool for deciding the satisfiability or validity of formulas using these theories. SMT solvers enable applications such as extended static checking, predicate abstraction, test case generation, bounded model checking over infinite domains, etc.
SMT solvers that perform searching over a large set of constraints need to maintain, update, and propagate truth assignments to atomic constraints (“atoms”) of a received formula being tested for satisfiability. Each new truth assignment may lead to additional constraint propagation, which is costly. The relative costliness depends on the constraint domain (real or integer linear arithmetic, bit-vectors, . . . , quantified formulas). For these expensive constraint domains, it is very desirable to limit case splits and constraint propagation to only cases that are relevant for solving the constraints.
Consider the following simplified example:a<1(a+b>0b<0)The example is a disjunction that requires either a to be less than 1, or requires a+b to be strictly greater than 0, but b to be less than 0. Assume that a and b range over integers, so that the legal values for a and b are the numbers . . . −2, −1, 0, 1, 2, . . . . The formula is satisfiable. A satisfying assignment is {a→0, b→3}. The assignment satisfies the first disjunction, but it cannot be used for the second disjunction. A satisfying assignment for the second disjunction is {a→2, b→−1}. The truth value of the atom a+b>0 is irrelevant when satisfying the first disjunction, and thus it is a waste of resources to satisfy either a+b>0 or the negation a+b≦0.
Conventional approaches to combining constraint solvers with efficient solvers for propositional satisfiability do not have mechanisms for avoiding the unnecessary propagation of irrelevant atoms. What is needed is a way to avoid such propagation, resulting in vast acceleration over the conventional approaches.